\begin{tabbing}
$M$.sframe($k$ sends $<$$l$,${\it tg}$$>$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}val(\=product{-}deq(IdLnk;Id;IdLnkDeq;IdDeq);\+
\\[0ex](($M$.2.2.2.2.2.2.2).1);
\\[0ex]$<$$l$, ${\it tg}$$>$;
\\[0ex]$x$,$L$.($\uparrow$deq{-}member(KindDeq;$k$;$L$)))
\-
\end{tabbing}